Effective Models of Polymorphism, Subtyping
and Recursion
(extended abstract)
John Mitchell, Department
of Computer Science, Stanford University, Stanford, CA 94305.
(Supported in part by NSF Grant
CCR-9303099 and a grant from the TRW Foundation.
Ramesh Viswanathan, Bell Laboratories, 101 Crawfords Corner Road,
Holmdel, NJ 07733. rv@research.att.com
(Supported by NSF Grant CCR-9303099.)
Abstract
We explore a class of models of polymorphism, subtyping and recursion
based on a combination of traditional recursion theory and simple
domain theory. A significant property of our primary model is that
types are coded by natural numbers using any index of their supremum
operator. This leads to a distinctive view of polymorphic functions
that has many of the usual parametricity properties. It also gives a
distinctive but entirely coherent interpretation of subtyping. An
alternate construction points out some peculiarities of computability
theory based on natural number codings. Specifically, the polymorphic
fixed point is computable by a single algorithm at all types when we
construct the model over untyped call-by-value lambda terms, but not
when we use G\"odel numbers for computable functions. This is
consistent with trends away from natural numbers in the field of
abstract recursion theory. Although our development and analysis of
each structure is completely elementary, both structures may be
obtained as the result of interpreting standard domain constructions
in effective models of constructive logic.